dtmc

//the length of the backoff stage
const int w=8;

// module for process 1
module carA
    backoffA : [0..w-1] init 0;

    //Indicate that A is sending a message, which is done whenever the backoff phase is 0
    sendA : [0..1] init 1;
    
    //make the model work for w upto 40
    //calculate the probability to reach a certain backoff state
    //The car sends a message whenever the transition to backoff state 0 is made
    [step] backoffA=0 -> 
			( w>0 ? 1 : 0 )*1/w:(backoffA'=0) & (sendA'=1) + 
			( w>1 ? 1 : 0 )*1/w:(backoffA'=1) & (sendA'=0) + 
			( w>2 ? 1 : 0 )*1/w:(backoffA'=2) & (sendA'=0) + 
			( w>3 ? 1 : 0 )*1/w:(backoffA'=3) & (sendA'=0) + 
			( w>4 ? 1 : 0 )*1/w:(backoffA'=4) & (sendA'=0) + 
			( w>5 ? 1 : 0 )*1/w:(backoffA'=5) & (sendA'=0) + 
			( w>6 ? 1 : 0 )*1/w:(backoffA'=6) & (sendA'=0) + 
			( w>7 ? 1 : 0 )*1/w:(backoffA'=7) & (sendA'=0) + 
			( w>8 ? 1 : 0 )*1/w:(backoffA'=8) & (sendA'=0) + 
			( w>9 ? 1 : 0 )*1/w:(backoffA'=9) & (sendA'=0) + 
			( w>10 ? 1 : 0 )*1/w:(backoffA'=10) & (sendA'=0) + 
			( w>11 ? 1 : 0 )*1/w:(backoffA'=11) & (sendA'=0) + 
			( w>12 ? 1 : 0 )*1/w:(backoffA'=12) & (sendA'=0) + 
			( w>13 ? 1 : 0 )*1/w:(backoffA'=13) & (sendA'=0) + 
			( w>14 ? 1 : 0 )*1/w:(backoffA'=14) & (sendA'=0) + 
			( w>15 ? 1 : 0 )*1/w:(backoffA'=15) & (sendA'=0) + 
			( w>16 ? 1 : 0 )*1/w:(backoffA'=16) & (sendA'=0) + 
			( w>17 ? 1 : 0 )*1/w:(backoffA'=17) & (sendA'=0) + 
			( w>18 ? 1 : 0 )*1/w:(backoffA'=18) & (sendA'=0) + 
			( w>19 ? 1 : 0 )*1/w:(backoffA'=19) & (sendA'=0);

    [step] backoffA=1 -> 1: (backoffA'=0) & (sendA'=1);
    [step] backoffA>1 -> 1: (backoffA'=backoffA-1) & (sendA'=0); 	
endmodule

// add further processes through renaming
module carB = carA[backoffA=backoffB, sendA=sendB] endmodule
module carC = carA[backoffA=backoffC, sendA=sendC] endmodule

rewards "succesfultransmission"
	sendA + sendB + sendC = 1 : 1;
endrewards

rewards "collision"
	sendA + sendB + sendC > 1 : 1;
endrewards
